\begin{tabbing}
$\forall$$T$, $A$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $i$:Id, $k$:Knd.
\\[0ex]Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ ($\neg$(locl("a") = $k$))
\\[0ex]$\Rightarrow$ R{-}Feasible(trigger1\=\{trigger:ut2, a:ut2, x:ut2\}\+
\\[0ex]($T$; $A$; $P$; $i$; $k$))
\-
\end{tabbing}